Inference at * 1 
Iof proof for Lemma assert of band:



1. p : 
2. q : 
  ((p  q))  ((p) & (q)) 

latex

 by ((((OnHyps [2;1] BoolInd) 
CollapseTHEN (Rewrite 
C(UnfoldC `band` 

C(UnORTHENC HigherC ifthenelse_evalC 
C(ORTHENC HigherC assert_evalC) 
C0))) 
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions	, P  Q, P  Q, True, ff, if b then t else f fi , tt, t  T, P & Q, p  q, b, P  Q, False, Unit, ,
Lemmas	false wf, true wf